!x:T. P(x) == x:T. P(x) & (y:T. P(y)  y = x) 

latex

---

clarification:

!x:T. P(x) == x:T. P(x) & (y:T. P(y)  y = x  T) 

latex

Definitions	x:A. B(x), P & Q, x:A. B(x), P  Q
FDL editor aliases	exists!